Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	0(#)	→ #
2:	x + #	→ x
3:	# + x	→ x
4:	0(x) + 0(y)	→ 0(x + y)
5:	0(x) + 1(y)	→ 1(x + y)
6:	1(x) + 0(y)	→ 1(x + y)
7:	1(x) + 1(y)	→ 0((x + y) + 1(#))
8:	x + (y + z)	→ (x + y) + z
9:	x - #	→ x
10:	# - x	→ #
11:	0(x) - 0(y)	→ 0(x - y)
12:	0(x) - 1(y)	→ 1((x - y) - 1(#))
13:	1(x) - 0(y)	→ 1(x - y)
14:	1(x) - 1(y)	→ 0(x - y)
15:	not(false)	→ true
16:	not(true)	→ false
17:	and(x,true)	→ x
18:	and(x,false)	→ false
19:	if(true,x,y)	→ x
20:	if(false,x,y)	→ y
21:	ge(0(x),0(y))	→ ge(x,y)
22:	ge(0(x),1(y))	→ not(ge(y,x))
23:	ge(1(x),0(y))	→ ge(x,y)
24:	ge(1(x),1(y))	→ ge(x,y)
25:	ge(x,#)	→ true
26:	ge(#,1(x))	→ false
27:	ge(#,0(x))	→ ge(#,x)
28:	val(l(x))	→ x
29:	val(n(x,y,z))	→ x
30:	min(l(x))	→ x
31:	min(n(x,y,z))	→ min(y)
32:	max(l(x))	→ x
33:	max(n(x,y,z))	→ max(z)
34:	bs(l(x))	→ true
35:	bs(n(x,y,z))	→ and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
36:	size(l(x))	→ 1(#)
37:	size(n(x,y,z))	→ (size(x) + size(y)) + 1(#)
38:	wb(l(x))	→ true
39:	wb(n(x,y,z))	→ and(if(ge(size(y),size(z)),ge(1(#),size(y) - size(z)),ge(1(#),size(z) - size(y))),and(wb(y),wb(z)))

There are 49 dependency pairs:


40:	0(x) +# 0(y)	→ 0#(x + y)
41:	0(x) +# 0(y)	→ x +# y
42:	0(x) +# 1(y)	→ x +# y
43:	1(x) +# 0(y)	→ x +# y
44:	1(x) +# 1(y)	→ 0#((x + y) + 1(#))
45:	1(x) +# 1(y)	→ (x + y) +# 1(#)
46:	1(x) +# 1(y)	→ x +# y
47:	x +# (y + z)	→ (x + y) +# z
48:	x +# (y + z)	→ x +# y
49:	0(x) -# 0(y)	→ 0#(x - y)
50:	0(x) -# 0(y)	→ x -# y
51:	0(x) -# 1(y)	→ (x - y) -# 1(#)
52:	0(x) -# 1(y)	→ x -# y
53:	1(x) -# 0(y)	→ x -# y
54:	1(x) -# 1(y)	→ 0#(x - y)
55:	1(x) -# 1(y)	→ x -# y
56:	GE(0(x),0(y))	→ GE(x,y)
57:	GE(0(x),1(y))	→ NOT(ge(y,x))
58:	GE(0(x),1(y))	→ GE(y,x)
59:	GE(1(x),0(y))	→ GE(x,y)
60:	GE(1(x),1(y))	→ GE(x,y)
61:	GE(#,0(x))	→ GE(#,x)
62:	MIN(n(x,y,z))	→ MIN(y)
63:	MAX(n(x,y,z))	→ MAX(z)
64:	BS(n(x,y,z))	→ AND(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
65:	BS(n(x,y,z))	→ AND(ge(x,max(y)),ge(min(z),x))
66:	BS(n(x,y,z))	→ GE(x,max(y))
67:	BS(n(x,y,z))	→ MAX(y)
68:	BS(n(x,y,z))	→ GE(min(z),x)
69:	BS(n(x,y,z))	→ MIN(z)
70:	BS(n(x,y,z))	→ AND(bs(y),bs(z))
71:	BS(n(x,y,z))	→ BS(y)
72:	BS(n(x,y,z))	→ BS(z)
73:	SIZE(n(x,y,z))	→ (size(x) + size(y)) +# 1(#)
74:	SIZE(n(x,y,z))	→ size(x) +# size(y)
75:	SIZE(n(x,y,z))	→ SIZE(x)
76:	SIZE(n(x,y,z))	→ SIZE(y)
77:	WB(n(x,y,z))	→ AND(if(ge(size(y),size(z)),ge(1(#),size(y) - size(z)),ge(1(#),size(z) - size(y))),and(wb(y),wb(z)))
78:	WB(n(x,y,z))	→ IF(ge(size(y),size(z)),ge(1(#),size(y) - size(z)),ge(1(#),size(z) - size(y)))
79:	WB(n(x,y,z))	→ GE(size(y),size(z))
80:	WB(n(x,y,z))	→ GE(1(#),size(y) - size(z))
81:	WB(n(x,y,z))	→ size(y) -# size(z)
82:	WB(n(x,y,z))	→ GE(1(#),size(z) - size(y))
83:	WB(n(x,y,z))	→ size(z) -# size(y)
84:	WB(n(x,y,z))	→ SIZE(z)
85:	WB(n(x,y,z))	→ SIZE(y)
86:	WB(n(x,y,z))	→ AND(wb(y),wb(z))
87:	WB(n(x,y,z))	→ WB(y)
88:	WB(n(x,y,z))	→ WB(z)

The approximated dependency graph contains 9 SCCs: {61}, {63}, {62}, {41-43,45-48}, {75,76}, {50-53,55}, {56,58-60}, {71,72} and {87,88}.

Consider the SCC {61}. There are no usable rules. By taking the AF π with π(GE) = 2 together with the lexicographic path order with empty precedence, rule 61 is strictly decreasing.

Consider the SCC {63}. There are no usable rules. By taking the AF π with π(MAX) = 1 and π(n) = [3] together with the lexicographic path order with empty precedence, rule 63 is strictly decreasing.

Consider the SCC {62}. There are no usable rules. By taking the AF π with π(MIN) = 1 and π(n) = [2] together with the lexicographic path order with empty precedence, rule 62 is strictly decreasing.

Consider the SCC {41-43,45-48}. The usable rules are {1-8}. The constraints could not be solved.

Consider the SCC {75,76}. There are no usable rules. By taking the AF π with π(SIZE) = 1 and π(n) = [1, 2] together with the lexicographic path order with empty precedence, the rules in {75,76} are strictly decreasing.

Consider the SCC {50-53,55}. The usable rules are {1,9-14}. By taking the AF π with π(-) = π(-#) = 1 together with the lexicographic path order with precedence 1 ≈ 0, the rules in {9-14} are weakly decreasing and the rules in {1,50-53,55} are strictly decreasing.

Consider the SCC {56,58-60}. There are no usable rules. The constraints could not be solved.

Consider the SCC {71,72}. There are no usable rules. By taking the AF π with π(BS) = 1 and π(n) = [2, 3] together with the lexicographic path order with empty precedence, the rules in {71,72} are strictly decreasing.

Consider the SCC {87,88}. There are no usable rules. By taking the AF π with π(WB) = 1 and π(n) = [2, 3] together with the lexicographic path order with empty precedence, the rules in {87,88} are strictly decreasing.

Tyrolean Termination Tool (0.15 seconds) --- May 4, 2006